from z3 import *

# Z 代表整数类型
Z = IntSort()

# f 代表函数类型，输入为整数，输出为整数
f = Function("f", Z, Z)

# 定义整数变量
x, y, x = Ints("x y x")

# 定义数组A
A = Array("A", Z, Z)

# Store(A, x, 3) 表示将A[x]设置为3
fml = Implies(x + 2 == y, f(Store(A, x, 3)[y - 2]) == f(y - x + 1))

# 求解
solve(Not(fml))
# > not solution

solve(fml)
# > [A = K(Int, 6), x = 0, y = 3]